Nuprl Definition : qadd 11,40

r + s
== if isint(r)
== then if isint(s) then r + s else let i,j = s in <(r * j) + ij> fi 
== else let p,q = r
== else in
== else if isint(s) then <p + (s * q), q> else let i,j = s in <(p * j) + (i * q), q * j> fi 
== fi  
latex



clarification:

r + s
== if isint(r;tt;ff)
== then if isint(s;tt;ff) then r + s else let i,j = s in <(r * j) + ij> fi 
== else let p,q = r
== else in
== else if isint(s;tt;ff) then <p + (s * q), q> else let i,j = s in <(p * j) + (i * q), q * j> fi 
== fi  
latex


Definitionsn * m, n + m, <ab>, let x,y = A in B(x;y), ff, tt, isint(z;a;b), if b then t else f fi 
FDL editor aliasesqadd

origin